<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofAsstGUI</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofAsstGUI";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofAsstGUI.RequestThreadStuff.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofAsstGUI.html" target="_top">Frames</a></li>
<li><a href="ProofAsstGUI.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li><a href="#nested_class_summary">Nested</a>&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.pa</div>
<h2 title="Class ProofAsstGUI" class="title">Class ProofAsstGUI</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.pa.ProofAsstGUI</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">ProofAsstGUI</span>
extends java.lang.Object</pre>
<div class="block">The <code>ProofAsstGUI</code> class is the main user interface for the mmj2 Proof
 Assistant feature.
 <p>
 A proof is represented in the GUI as a single text area, and the GUI knows
 nothing about the contents inside; all work on the proof is done elsewhere
 via mmj.pa.ProofAsst.java.
 <p>
 Note: ProofAsstGUI is single-threaded in the ProofAsst process which is
 triggered in BatchMMJ2. The RunParm that triggers ProofAsstGUI does not
 terminate until ProofAsstGUI terminates.
 <p>
 The main issues dealt with in the GUI have to do with doing all of the screen
 updating code on the Java event thread. Unification is performed using a
 separate thread which "calls back" to ProofAsstGUI when/if the Unificatin
 process is complete. (As of February 2006, the longest theorem unification
 computation is around 1/2 second.)</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== NESTED CLASS SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="nested_class_summary">
<!--   -->
</a>
<h3>Nested Class Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Nested Class Summary table, listing nested classes, and an explanation">
<caption><span>Nested Classes</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Class and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>class&nbsp;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.RequestThreadStuff.html" title="class in mmj.pa">ProofAsstGUI.RequestThreadStuff</a></strong></code>&nbsp;</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#ProofAsstGUI()">ProofAsstGUI</a></strong>()</code>
<div class="block">Default constructor used only in test mode when ProofAsstGUI invoked
 directly from command line.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#ProofAsstGUI(mmj.pa.ProofAsst, mmj.pa.ProofAsstPreferences, mmj.tl.TheoremLoader)">ProofAsstGUI</a></strong>(<a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst,
            <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
            <a href="../../mmj/tl/TheoremLoader.html" title="class in mmj.tl">TheoremLoader</a>&nbsp;theoremLoader)</code>
<div class="block">Normal constructor for setting up ProofAsstGUI.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#cancelRequestAction()">cancelRequestAction</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#getCurrProofMaxSeq()">getCurrProofMaxSeq</a></strong>()</code>
<div class="block">Get sequence number of Proof Worksheet theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>javax.swing.JFrame</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#getMainFrame()">getMainFrame</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#main(java.lang.String[])">main</a></strong>(java.lang.String[]&nbsp;args)</code>
<div class="block">Test code to invoke GUI from command line.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#newGeneralSearch(java.lang.String)">newGeneralSearch</a></strong>(java.lang.String&nbsp;s)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#refineAndShowResults()">refineAndShowResults</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#reshowProofAsstGUI()">reshowProofAsstGUI</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#reshowSearchOptions()">reshowSearchOptions</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#reshowSearchResults()">reshowSearchResults</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#searchAndShowResults()">searchAndShowResults</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#searchOptionsMinusButton()">searchOptionsMinusButton</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#searchOptionsPlusButton()">searchOptionsPlusButton</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#searchResultsMinusButton()">searchResultsMinusButton</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#searchResultsPlusButton()">searchResultsPlusButton</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#setCurrProofMaxSeq(int)">setCurrProofMaxSeq</a></strong>(int&nbsp;currProofMaxSeq)</code>
<div class="block">Set sequence number of Proof Worksheet theorem.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#setCursorToStartOfMessageArea()">setCursorToStartOfMessageArea</a></strong>()</code>
<div class="block">Positions the input caret to start of message text area and scrolls
 viewport to ensure that the start of the message text area is visible.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#showMainFrame()">showMainFrame</a></strong>()</code>
<div class="block">Show the GUI's main frame (screen).</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#startRequestAction(mmj.pa.ProofAsstGUI.Request)">startRequestAction</a></strong>(mmj.pa.ProofAsstGUI.Request&nbsp;r)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#unifyWithSearchChoice(mmj.pa.StepRequest)">unifyWithSearchChoice</a></strong>(<a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsstGUI.html#unifyWithStepSelectorChoice(mmj.pa.StepRequest)">unifyWithStepSelectorChoice</a></strong>(<a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)</code>&nbsp;</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofAsstGUI()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>ProofAsstGUI</h4>
<pre>public&nbsp;ProofAsstGUI()</pre>
<div class="block">Default constructor used only in test mode when ProofAsstGUI invoked
 directly from command line.</div>
</li>
</ul>
<a name="ProofAsstGUI(mmj.pa.ProofAsst, mmj.pa.ProofAsstPreferences, mmj.tl.TheoremLoader)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofAsstGUI</h4>
<pre>public&nbsp;ProofAsstGUI(<a href="../../mmj/pa/ProofAsst.html" title="class in mmj.pa">ProofAsst</a>&nbsp;proofAsst,
            <a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
            <a href="../../mmj/tl/TheoremLoader.html" title="class in mmj.tl">TheoremLoader</a>&nbsp;theoremLoader)</pre>
<div class="block">Normal constructor for setting up ProofAsstGUI.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofAsst</code> - ProofAsst object</dd><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>theoremLoader</code> - mmj.tl.TheoremLoader object</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="getCurrProofMaxSeq()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCurrProofMaxSeq</h4>
<pre>public&nbsp;int&nbsp;getCurrProofMaxSeq()</pre>
<div class="block">Get sequence number of Proof Worksheet theorem.
 <p>
 Equals MObj.seq if proof theorem already exists. Otherwise, set to
 LOC_AFTER stmt sequnce + 1 if LOC_AFTER input (else Integer.MAX_VALUE).</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>currProofMaxSeq number of Proof Worksheet theorem.</dd></dl>
</li>
</ul>
<a name="setCurrProofMaxSeq(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setCurrProofMaxSeq</h4>
<pre>public&nbsp;void&nbsp;setCurrProofMaxSeq(int&nbsp;currProofMaxSeq)</pre>
<div class="block">Set sequence number of Proof Worksheet theorem.
 <p>
 Equals MObj.seq if proof theorem already exists. Otherwise, set to
 LOC_AFTER stmt sequnce + 1 if LOC_AFTER input (else Integer.MAX_VALUE).</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>currProofMaxSeq</code> - number of Proof Worksheet theorem.</dd></dl>
</li>
</ul>
<a name="unifyWithStepSelectorChoice(mmj.pa.StepRequest)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unifyWithStepSelectorChoice</h4>
<pre>public&nbsp;void&nbsp;unifyWithStepSelectorChoice(<a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)</pre>
</li>
</ul>
<a name="newGeneralSearch(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>newGeneralSearch</h4>
<pre>public&nbsp;boolean&nbsp;newGeneralSearch(java.lang.String&nbsp;s)</pre>
</li>
</ul>
<a name="searchAndShowResults()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>searchAndShowResults</h4>
<pre>public&nbsp;boolean&nbsp;searchAndShowResults()</pre>
</li>
</ul>
<a name="refineAndShowResults()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>refineAndShowResults</h4>
<pre>public&nbsp;boolean&nbsp;refineAndShowResults()</pre>
</li>
</ul>
<a name="reshowSearchOptions()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>reshowSearchOptions</h4>
<pre>public&nbsp;boolean&nbsp;reshowSearchOptions()</pre>
</li>
</ul>
<a name="reshowSearchResults()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>reshowSearchResults</h4>
<pre>public&nbsp;boolean&nbsp;reshowSearchResults()</pre>
</li>
</ul>
<a name="reshowProofAsstGUI()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>reshowProofAsstGUI</h4>
<pre>public&nbsp;boolean&nbsp;reshowProofAsstGUI()</pre>
</li>
</ul>
<a name="searchOptionsPlusButton()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>searchOptionsPlusButton</h4>
<pre>public&nbsp;boolean&nbsp;searchOptionsPlusButton()</pre>
</li>
</ul>
<a name="searchOptionsMinusButton()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>searchOptionsMinusButton</h4>
<pre>public&nbsp;boolean&nbsp;searchOptionsMinusButton()</pre>
</li>
</ul>
<a name="searchResultsPlusButton()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>searchResultsPlusButton</h4>
<pre>public&nbsp;boolean&nbsp;searchResultsPlusButton()</pre>
</li>
</ul>
<a name="searchResultsMinusButton()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>searchResultsMinusButton</h4>
<pre>public&nbsp;boolean&nbsp;searchResultsMinusButton()</pre>
</li>
</ul>
<a name="getMainFrame()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMainFrame</h4>
<pre>public&nbsp;javax.swing.JFrame&nbsp;getMainFrame()</pre>
</li>
</ul>
<a name="unifyWithSearchChoice(mmj.pa.StepRequest)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unifyWithSearchChoice</h4>
<pre>public&nbsp;void&nbsp;unifyWithSearchChoice(<a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest)</pre>
</li>
</ul>
<a name="startRequestAction(mmj.pa.ProofAsstGUI.Request)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>startRequestAction</h4>
<pre>public&nbsp;boolean&nbsp;startRequestAction(mmj.pa.ProofAsstGUI.Request&nbsp;r)</pre>
</li>
</ul>
<a name="cancelRequestAction()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>cancelRequestAction</h4>
<pre>public&nbsp;boolean&nbsp;cancelRequestAction()</pre>
</li>
</ul>
<a name="setCursorToStartOfMessageArea()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setCursorToStartOfMessageArea</h4>
<pre>public&nbsp;void&nbsp;setCursorToStartOfMessageArea()</pre>
<div class="block">Positions the input caret to start of message text area and scrolls
 viewport to ensure that the start of the message text area is visible.
 <p>
 This is called only after updates to an existing AuxFrameGUI screen. It
 is automatically invoked during the initial display sequence of events..</div>
</li>
</ul>
<a name="showMainFrame()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>showMainFrame</h4>
<pre>public&nbsp;void&nbsp;showMainFrame()</pre>
<div class="block">Show the GUI's main frame (screen).</div>
</li>
</ul>
<a name="main(java.lang.String[])">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>main</h4>
<pre>public static&nbsp;void&nbsp;main(java.lang.String[]&nbsp;args)</pre>
<div class="block">Test code to invoke GUI from command line.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>args</code> - String array holding command line parms</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofAsstGUI.RequestThreadStuff.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofAsstGUI.html" target="_top">Frames</a></li>
<li><a href="ProofAsstGUI.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li><a href="#nested_class_summary">Nested</a>&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
